Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    ap(ap(f,x),x)  → ap(ap(x,ap(f,x)),ap(ap(cons,x),nil))
2:    ap(ap(ap(foldr,g),h),nil)  → h
3:    ap(ap(ap(foldr,g),h),ap(ap(cons,x),xs))  → ap(ap(g,x),ap(ap(ap(foldr,g),h),xs))
There are 7 dependency pairs:
4:    AP(ap(f,x),x)  → AP(ap(x,ap(f,x)),ap(ap(cons,x),nil))
5:    AP(ap(f,x),x)  → AP(x,ap(f,x))
6:    AP(ap(f,x),x)  → AP(ap(cons,x),nil)
7:    AP(ap(f,x),x)  → AP(cons,x)
8:    AP(ap(ap(foldr,g),h),ap(ap(cons,x),xs))  → AP(ap(g,x),ap(ap(ap(foldr,g),h),xs))
9:    AP(ap(ap(foldr,g),h),ap(ap(cons,x),xs))  → AP(g,x)
10:    AP(ap(ap(foldr,g),h),ap(ap(cons,x),xs))  → AP(ap(ap(foldr,g),h),xs)
The approximated dependency graph contains one SCC: {4,6,8-10}.
Tyrolean Termination Tool  (0.07 seconds)   ---  May 3, 2006